#include <alloc.h>
#include <ctype.h>
#include "beh.h"
//#include "pamet.h"
#include "unikat.h"
#include "qconst.h"
#include "ce_chars.h"
//#include "q_io.h"

int Bunikat=0;//rika, zda se detekuji duplicitni hrany a nedochazi k jejich vytvareni
int Bgraflog=0;//rika, zda se do logu zapisuje graf v kazde fazi pred cistenim
int Bcesty=0;//rika, zda se log grafu pise jako cesty, nebo po usecich
int Bprazdnygraf=0;

Qstrom *NIL;

struct Log{
  FILE *f;
  int fz;
  int p;
};

static Log log;
static Ustrom *unik;
static Qhrana *S,*K;
static unsigned long stari;

static int memerr;
#define ERR memerr=1
#define MEM if(memerr)break
#define MER if(memerr)return
#define MERR QERR<<STR_NOTENOUGHMEMORY<<endln
//#define malo_pameti(a) if(!a)memerr=1

void serad_uzly(Qhrana *s){
  Qhrana *p,*q,*r;
  p=q=s;
  while(p){
    p->npouz(1);
    if(p->vvetev2()&&!p->vvetev2()->vpouz())
      {q->ndalsi(p->vvetev2());q=q->dal();}
    r=p->vretez2();
    if(r){
      r=r->vretez1();
      while(r&&r->vpouz()) r=r->vvetev1();
      if(!r) {q->ndalsi(p->vretez2());q=q->dal();}
      else if(r->vretez2()->vpouz()){
        printf("CHYBA: spatne razeni uzlu");
        exit(-1);
      }
    }
    p=p->dal();
  }
  p=s;
  while(p){
    p->nurov(0);
    p->npouz(0);
    p=p->dal();
  }
  stari=1;
}

void zrus_seznam_promennych(Bpromsez *s){
  while(s){
    Bpromsez *p=s;
    s=s->dal;
    delete p;
  }
}

void seznam_promennych_rek(Bpromsez **s,Qstrom *u){
  if(u->vkonst()==_Ldekompozice){
    Bpromsez **p=s;
    while(*p&&strcmp((*p)->jmeno,u->vdesint()->vobsah())) p=&((*p)->dal);
    if(*p==NULL){
      Bpromsez *q=*p=new Bpromsez;
      if(!q) ERR;
      else{
        q->obsah=NULL;
        q->jmeno=u->vdesint()->vobsah();
        q->dal=NULL;
      }
    }
  }else if(u->vkonst()){
    Bpromsez **p=s;
    while(*p&&strcmp((*p)->jmeno,u->vobsah())) p=&((*p)->dal);
    if(*p==NULL){
      Bpromsez *q=*p=new Bpromsez;
      if(!q) ERR;
      else{
        q->obsah=NULL;
        q->jmeno=u->vobsah();
        q->dal=NULL;
      }
    }
  }
  if(u->vbratr()) seznam_promennych_rek(s,u->vbratr());
  if(u->vsyn()) seznam_promennych_rek(s,u->vsyn());
}

void seznam_promennych(Bpromsez **s,Qhrana *u){
  while(u){
    seznam_promennych_rek(s,u->vstrom());
    MEM;
    u=u->vretez1();
  }
  if(memerr) zrus_seznam_promennych(*s);
}

Bpromsez *obsah(char *o,Bpromsez *s){
  while(strcmp(s->jmeno,o)) s=s->dal;
  return s;
}

//Zpet k programu:

void kopiruj(Qstrom *co,Qstrom *&novy,Qstrom *&konec,Bpromsez *ps){
  Qstrom *n=NULL,*k=NULL,*p,*q;
  switch(co->vkonst()){
    case _Latom:
      novy=new Qstrom(co->vjmeno(),co->vkonst());
      if(!novy) ERR;
      else{
        novy->vjmeno()->zvys();
        co=co->vsyn();
        if(co){
          while(co&&!n){
            kopiruj(co,p,k,ps);
            n=p;
            co=co->vbratr();
          }
          while(co){
            kopiruj(co,p,q,ps);
            if(p){
              k->nbratr(p);
              k=q;
            }
            co=co->vbratr();
          }
          if(memerr){
            if(n) n->pocminus();
            novy->pocminus();
            novy=NULL;
          }else novy->nsyn(n);
        }
      }
      konec=novy;
      break;
    case _Latomovapromenna:
      p=obsah(co->vobsah(),ps)->obsah;
      novy=new Qstrom(p->vjmeno(),p->vkonst());
      if(!novy) ERR;
      else{
        novy->vjmeno()->zvys();
        co=co->vsyn();
        if(co){
          while(co&&!n){
            kopiruj(co,p,k,ps);
            n=p;
            co=co->vbratr();
          }
          while(co){
            kopiruj(co,p,q,ps);
            if(p){
              k->nbratr(p);
              k=q;
            }
            co=co->vbratr();
          }
          if(memerr){
            if(n) n->pocminus();
            novy->pocminus();
            novy=NULL;
          }else novy->nsyn(n);
        }
      }
      konec=novy;
      break;
    case _Lstromovapromenna:
      p=obsah(co->vobsah(),ps)->obsah;
      novy=new Qstrom(p->vjmeno(),p->vkonst());
      if(!novy) ERR;
      else{
        novy->vjmeno()->zvys();
        if(p->vsyn()) novy->nsyn(p->adsyn());
      }
      konec=novy;
      break;
    case _Lseznamovapromenna:
      p=obsah(co->vobsah(),ps)->obsah;
      if(p!=NIL){
        novy=new Qstrom(p->vjmeno(),p->vkonst());
        if(!novy){ ERR; konec=NULL; }
        else{
          novy->vjmeno()->zvys();
          if(p->vsyn()) novy->nsyn(p->adsyn());
          k=novy;
          p=p->vbratr();
          while(p){
            n=new Qstrom(p->vjmeno(),p->vkonst());
            if(!n){
              ERR;
              novy->pocminus();
              novy=k=NULL;
              break;
            }
            n->vjmeno()->zvys();
            if(p->vsyn()) n->nsyn(p->adsyn());
            k->nbratr(n);
            k=n;
            p=p->vbratr();
          }
          konec=k;
        }
      }else novy=NULL;
      break;
    case _Ldekompozice:
      string s1=" ",s2;
      int i=0;
      strcpy(s2,obsah(co->vdesint()->vobsah(),ps)->obsah->vobsah());
      s1[0]=s2[i++];
      k=novy=new Qstrom(s1,_Latom);
      if(!novy) ERR;
      else while(s2[i]){
        s1[0]=s2[i++];
        n=new Qstrom(s1,_Latom);
        if(!n){
          ERR;
          novy->pocminus();
          novy=k=NULL;
          break;
        }
        k->nbratr(n);
        k=n;
      }
      konec=k;
      break;
  }
}

int un_test(Qhrana *n,Qhrana *u,Qhrana *k,int i=0){
  Qhrana *p=k;
  while(u){
    if(unik?n->vstrom()==u->vstrom():!Qstrom_cmp(n->vstrom(),u->vstrom())){
      Qhrana *q;
      unsigned long s=u->vurov();
      if(n->vretez1()){
        Qhrana *q;
        unsigned long s=u->vurov();
        for(q=u->vretez1()?u->vretez1()->vretez2():K;q;q=q->vvetev2()) if(q->vurov()<=s&&q!=u) break;
        if(!q){
          if(i) for(q=u->vretez2()->vretez1();q;q=q->vvetev1()) if(q->vurov()<=s&&q!=u) break;
          if(!q||!i) if(un_test(n->vretez1(),u->vretez1(),k,1)) return 1;
        }
      }else{
        if(i) for(q=u->vretez2()->vretez1();q;q=q->vvetev1()) if(q->vurov()<=s&&q!=u) break;
        if(!q||!i){
          while(p&&p!=u) p=p->vvetev2();
          if(p) return 1;
          p=k;
        }
      }
    }
    u=u->vvetev1();
  }
  return 0;
}

void pridej_hranu(Qhrana *co,Bpromsez *ps,Qhrana *poc,Qhrana *kon,Qhrana *kam){
  Qhrana *nove,*nk,*h;
  Qstrom *p,*q;
  int pridat=1;
  kopiruj(co->vstrom(),p,q,ps);
  MER;
  if(unik) unik->unikat(p);
  nove=nk=new Qhrana(p);
  if(!nove){
    ERR;
    if(unik&&p->pocitadlo()==1) unik->zrus(p);
    p->pocminus();
    return;
  }
  nove->nurov(stari);
  co=co->vretez1();
  while(co){
    kopiruj(co->vstrom(),p,q,ps);
    if(memerr){
      if(unik){
        h=nove;
        while(h){
          if(h->vstrom()->pocitadlo()==1) unik->zrus(h->vstrom());
          h=h->vretez1();
        }
      }
      nove->pocminus();
    }
    if(unik) unik->unikat(p);
    h=new Qhrana(p);
    if(!h){
      ERR;
      if(unik&&p->pocitadlo()==1) unik->zrus(p);
      p->pocminus();
      if(unik){
        h=nove;
        while(h){
          if(h->vstrom()->pocitadlo()==1) unik->zrus(h->vstrom());
          h=h->vretez1();
        }
      }
      nove->pocminus();
    }
    h->nurov(stari);
    nk->nretez1(h);
    h->ndalsi(nk);
    h->nretez2(nk);
    nk=h;
    co=co->vretez1();
  }
  if(Bunikat){//jsou-li zakazany duplicitni hrany
    Qhrana *p1,*p2;
    p1=poc->vretez2()?poc->vretez2()->vretez1():S;
    p2=kon->vretez1()?kon->vretez1()->vretez2():K;
    pridat=!un_test(nove,p1,p2);
  }
  log.p=pridat;
  if(pridat){
    nove->nretez2(poc->vretez2());
    nove->nvetev1(poc->vvetev1());
    poc->nvetev1(nove);
    nk->nretez1(kon->vretez1());
    nk->nvetev2(kon->vvetev2());
    kon->nvetev2(nk);
    nove->ndalsi(kam->dal());
    kam->ndalsi(nk);
    stari++;
  }else{
    if(unik){
      h=nove;
      while(h){
        if(h->vstrom()->pocitadlo()==1) unik->zrus(h->vstrom());
        h=h->vretez1();
      }
    }
    nove->pocminus();
  }
}

int zapis_strom(Qstrom *u,Bpromsez *ps,int c){
  Qstrom *p=u;
  switch(u->vkonst()){
    char *s;
    int i;
    case _Ldekompozice:
      if(c) fprintf(log.f,",");
      s=obsah(u->vdesint()->vobsah(),ps)->obsah->vobsah();
      i=0;
      fprintf(log.f,"%c",s[i++]);
      while(s[i]) fprintf(log.f,",%c",s[i++]);
      break;
    case _Latomovapromenna:
      u=obsah(u->vobsah(),ps)->obsah;
      goto skok;
    case _Lstromovapromenna:
      u=obsah(u->vobsah(),ps)->obsah;
      p=u;
    skok:
    case _Latom:
      if(c) fprintf(log.f,",");
      fprintf(log.f,"%s",u->vobsah());
      u=p;
      u=u->vsyn();
      if(u){
        Qstrom *p=NULL;
        while(!p){
          if(u->vkonst()==_Lseznamovapromenna){
            p=obsah(u->vobsah(),ps)->obsah;
            if(p==NIL){
              u=u->vbratr();
              p=NULL;
              if(!u) break;
            }else p=u;
          }else p=u;
        }
        if(p){
          fprintf(log.f,"(");
          while(p&&!zapis_strom(p,ps,0))p=p->vbratr();
          if(p) p=p->vbratr();
          while(p){
            while(p&&!zapis_strom(p,ps,1))p=p->vbratr();
            if(p) p=p->vbratr();
          }
          fprintf(log.f,")");
        }
      }
      break;
    case _Lseznamovapromenna:
      u=obsah(u->vobsah(),ps)->obsah;
      if(u==NIL) return 0;
      if(c) fprintf(log.f,",");
      zapis_strom(u,ps,0);
      u=u->vbratr();
      while(u){
        zapis_strom(u,ps,1);
        u=u->vbratr();
      }
      break;
    case _Lnul:
      if(c) fprintf(log.f,",");
      fprintf(log.f,"-NUL-");
      break;
  }
  return 1;
}

void zapis_retez(Qhrana *h,Bpromsez *ps){
  zapis_strom(h->vstrom(),ps,0);
  h=h->vretez1();
  while(h){
    fprintf(log.f," + ");
    zapis_strom(h->vstrom(),ps,0);
    h=h->vretez1();
  }
}

void zapis_log(Qpravidlo *pr,Bpromsez *ps){
  fprintf(log.f,"(%i.%i) ",log.fz,pr->vid());
  zapis_retez(pr->levyretez(),ps);
  fprintf(log.f," == ");
  zapis_retez(pr->pravyretez(),ps);
  fprintf(log.f," .\n");
}

void lwr(char *s){
  while(*s){
    fputc(tolower(*s),log.f);
    s++;
  }
}

void zapis_strom(Qstrom *s,int lw,int c=1){
  if(c) fprintf(log.f,",");
  if(lw) lwr(s->vobsah());
  else fprintf(log.f,"%s",s->vobsah());
  Qstrom *t=s->vsyn();
  if(t){
    fprintf(log.f,"(");
    zapis_strom(t,lw,0);
    t=t->vbratr();
    while(t){
      zapis_strom(t,lw);
      t=t->vbratr();
    }
    fprintf(log.f,")");
  }
}

struct Blg{
  Blg *d;
  Qhrana *h;
};

void zapis_cesty(Blg *h,Blg *s){
  Qhrana *d=h->h->vretez1();
  if(d){
    Blg *p=new Blg;
    if(!p){ ERR; return; }
    h->d=p;
    do{
      p->d=NULL;
      p->h=d;
      zapis_cesty(p,s);
      d=d->vvetev1();
    }while(d);
    delete(p);
  }else{
    zapis_strom(s->h->vstrom(),s->h->vpouz(),0);
    s=s->d;
    while(s){
      fprintf(log.f," + ");
      zapis_strom(s->h->vstrom(),s->h->vpouz(),0);
      s=s->d;
    }
    fprintf(log.f,"\n");
  }
}

void zapis_log_grafu(Qhrana *h){
  Blg *p=new Blg;
  if(!p){ ERR; return; }
  if(Bcesty){
    while(h){
      p->d=NULL;
      p->h=h;
      zapis_cesty(p,p);
      h=h->vvetev1();
    }
    delete p;
  }else{
    Blg *pk=p;
    p->d=NULL;
    p->h=h;
    unsigned long n=1,v,k=0;
    h->nurov(n);
    while(p){
      h=p->h;
      v=h->vurov();
      while(h){
        fprintf(log.f,"-%lu- ",v);
        zapis_strom(h->vstrom(),h->vpouz(),0);
        Qhrana *d=h->vretez1();
        while(d&&!d->vvetev1()&&!d->vretez2()->vvetev2()){
          fprintf(log.f," + ");
          zapis_strom(d->vstrom(),d->vpouz(),0);
          d=d->vretez1();
        }
        if(d){
          if(!d->vurov()){
	    d->nurov(++n);
            pk->d=new Blg;
            if(!pk->d) ERR;
	    else{
              pk=pk->d;
              pk->d=NULL;
              pk->h=d;
            }
          }
          fprintf(log.f," -%lu-\n",d->vurov());
        }else{
          if(!k) k=++n;
          fprintf(log.f," -%lu-\n",k);
        }
        h=h->vvetev1();
      }
      Blg *q=p;
      p=p->d;
      delete q;
    }
  }
}

#define isid(ch) (isalnum_ce(ch)||(ch)=='_') // changed PH June 4 (unif. of decomp.)

/*int isid(char ch) {
	int r = isalnum(ch);
	printf("%c %d\n", ch, r);
	return r;
} /**/

void unifikuj(Bsezsez *ss,Bpromsez *ps,Qhrana *koren1,Qhrana *koren2,Qhrana *lkonec,Qpravidlo *pr,int &uzito){
  Bunif *unf=NULL;
  dal://unifikace zatim uspesna
  if(ss){
    if(ss->u1){
      switch(ss->u1->vkonst()){
        Bunif *pun;
        Bpromsez *p;
//        Bsezsez *o;
//        int nove;
        case _Latom:
          if(ss->u2==NULL||strcmp(ss->u1->vobsah(),ss->u2->vobsah())) goto zpet;
          pun=new Bunif;
          if(!pun){ ERR; goto zpet; }
          pun->o=new Bsezsez;
          if(!pun->o){ delete pun; ERR; goto zpet; }
          pun->konst=_Latom;
          pun->p=NULL;
          pun->zpet=unf;
          unf=pun;
          pun->o->u1=ss->u1->vsyn();
          pun->o->u2=ss->u2->vsyn();
          pun->o->dal=ss->dal;
          ss->u1=ss->u1->vbratr();
          ss->u2=ss->u2->vbratr();
          ss->dal=pun->o;
          pun->o=ss;
          goto dal;
        case _Latomovapromenna:
          if(ss->u2==NULL) goto zpet;
          p=obsah(ss->u1->vobsah(),ps);
          pun=new Bunif;
          if(!pun){ ERR; goto zpet; }
          pun->konst=_Latomovapromenna;
          pun->p=NULL;
          pun->zpet=unf;
          unf=pun;
          if(p->obsah){
            if(strcmp(p->obsah->vobsah(),ss->u2->vobsah())) {unf=pun->zpet;delete pun;goto zpet;}
          }else{
            pun->p=p;
	    pun->p->obsah=ss->u2;
          }
          pun->o=new Bsezsez;
          if(!pun->o){ ERR; if(pun->p)p->obsah=NULL; unf=pun->zpet; delete pun; goto zpet; }
          pun->o->u1=ss->u1->vsyn();
          pun->o->u2=ss->u2->vsyn();
          pun->o->dal=ss->dal;
          ss->u1=ss->u1->vbratr();
          ss->u2=ss->u2->vbratr();
          ss->dal=pun->o;
          pun->o=ss;
          goto dal;
        case _Lstromovapromenna:
          if(ss->u2==NULL) goto zpet;
          p=obsah(ss->u1->vobsah(),ps);
          pun=new Bunif;
          if(!pun){ ERR; goto zpet; }
          pun->konst=_Lstromovapromenna;
          pun->zpet=unf;
          unf=pun;
          if(p->obsah){
            if(strcmp(p->obsah->vobsah(),ss->u2->vobsah())) {unf=pun->zpet;delete pun;goto zpet;}
            pun->o=new Bsezsez;
            if(!pun->o){ ERR; unf=pun->zpet; delete pun; goto zpet; }
            pun->p=NULL;
            pun->o->u1=p->obsah->vsyn();
            pun->o->u2=ss->u2->vsyn();
            pun->o->dal=ss->dal;
            ss->u1=ss->u1->vbratr();
            ss->u2=ss->u2->vbratr();
            ss->dal=pun->o;
            pun->o=ss;
          }else{
            pun->p=p;
            pun->p->obsah=ss->u2;
            ss->u1=ss->u1->vbratr();
            ss->u2=ss->u2->vbratr();
          }
          goto dal;
        case _Lseznamovapromenna:
          p=obsah(ss->u1->vobsah(),ps);
          pun=new Bunif;
          if(!pun){ ERR; goto zpet; }
          pun->o=ss;
          pun->konst=_Lseznamovapromenna;
          pun->zpet=unf;
          pun->lok.s=new Bsezunif;
          if(!pun->lok.s){ ERR; delete pun; goto zpet; }
          unf=pun;
          ss->u1=ss->u1->vbratr();
          if(p->obsah){
            pun->p=NULL;
            Qstrom *q=p->obsah;
            pun->lok.s->s=ss->dal;
            while(q&&ss->u2){
              if(strcmp(q->vobsah(),ss->u2->vobsah())) goto zpet;
              pun->o=new Bsezsez;
              if(!pun->o){ ERR; goto zpet; }
              pun->o->u1=q->vsyn();
              pun->o->u2=ss->u2->vsyn();
              pun->o->dal=ss->dal;
              ss->u2=ss->u2->vbratr();
              ss->dal=pun->o;
              q=q->vbratr();
              pun->o=ss;
            }
            if(!q) goto dal;
            goto zpet;
          }else{
            pun->p=p;
            pun->lok.s->q=NIL;
            pun->lok.s->u=NIL;
            pun->p->obsah=pun->lok.s->q;
            pun->lok.s->ss1=ss->u1;
            pun->lok.s->ss2=ss->u2;
            goto dal;
          }
        case _Ldekompozice:
	  // !!!
          if(ss->u2==NULL) goto zpet;
          p=obsah(ss->u1->vdesint()->vobsah(),ps);
          ss->u1=ss->u1->vbratr();
          if(p->obsah){
            char *c=p->obsah->vobsah();
	    //printf("1 %s\n", c);
            while(*c&&ss->u2){
              if(ss->u2->vsyn()||strlen(ss->u2->vobsah())!=1||*(ss->u2->vobsah())!=*c) goto zpet;
              ss->u2=ss->u2->vbratr();
              c++;
            }
            if(*c) goto zpet;
            goto dal;
          }else{
            pun=new Bunif;
            if(!pun){ ERR; goto zpet; }
            pun->o=ss;
            pun->konst=_Ldekompozice;
            pun->p=p;
            pun->zpet=unf;
            pun->lok.d=new Bdesunif;
            if(!pun->lok.d){ ERR; delete pun; goto zpet; }
            unf=pun;
            pun->lok.d->q=new Qstrom("",_Latom);
            if(!pun->lok.d->q){ ERR; delete pun->lok.d; unf=pun->zpet; delete pun; goto zpet; }
            pun->p->obsah=pun->lok.d->q;
            pun->lok.d->i=0;
            pun->lok.d->s[pun->lok.d->i]=0;
            if(ss->u2&&!ss->u2->vsyn()&&strlen(ss->u2->vobsah())==1){
              pun->lok.d->s[pun->lok.d->i++]=*(ss->u2->vobsah());
              pun->lok.d->s[pun->lok.d->i]=0;
              pun->lok.d->q->nobsah(pun->lok.d->s);
	      //fprintf(stderr, "2 %s %d\n", pun->lok.d->s, strlen(pun->lok.d->s));
              ss->u2=ss->u2->vbratr();
              pun->lok.d->ss1=ss->u1;
              pun->lok.d->ss2=ss->u2;
              goto dal;
            }
            pun->lok.d->q->pocminus();
            pun->p->obsah=NULL;
          }
          goto zpet;
      }
    }else if(ss->u2) goto zpet;
    else{
      if(ss->dal){
        Bunif *pun=new Bunif;
        if(!pun){ ERR; goto zpet; }
        pun->o=ss;
        pun->konst=-1;
        pun->zpet=unf;
        pun->lok.k=new Bkrokunif;
        if(!pun->lok.k){ ERR; delete pun; goto zpet; }
        unf=pun;
        pun->lok.k->p1=ss->dal->u1;
        pun->lok.k->p2=ss->dal->u2;
        ss=ss->dal;
        goto dal;
      }else{
        ss=ss->dal;
        goto dal;
      }
    }
  }else{// unifikace hrany hotova, uspesna
    Qhrana *k1=koren1;
    koren1=koren1->vretez1();
    if(koren1){
      Qhrana *p=koren2->vretez1();
      ss=new Bsezsez;
      if(!ss) ERR;
      else{
        ss->u1=koren1->vstrom();
        ss->dal=NULL;
        while(p){
          ss->u2=p->vstrom();
          int puzito=0;
          Qstrom *p1=ss->u1;
          unifikuj(ss,ps,koren1,p,lkonec,pr,puzito);
          ss->u1=p1;
          if(puzito) uzito=1;
          p=p->vvetev1();
        }
        delete ss;
      }
    }else{// unifikace pravidla uspesna, lze jej pouzit
      if(!pr->podminka()||pr->podminka()->over(ps)){
        pridej_hranu(pr->pravyretez(),ps,lkonec,koren2,lkonec);
        if(log.f&&log.p) zapis_log(pr,ps);
        uzito=1;
      }
    }
    if(uzito) koren2->npouz(1);
    koren1=k1;
  }
  zpet://neuspech unifikace
  if(unf){
    Bunif *pun;
    switch(unf->konst){
      case _Latomovapromenna:
        if(unf->p) unf->p->obsah=NULL;
      case _Latom:
        ss=unf->o;
        unf->o=ss->dal;
        ss->dal=ss->dal->dal;
        delete unf->o;
        break;
      case _Lstromovapromenna:
        if(unf->p) unf->p->obsah=NULL;
        else{
          ss=unf->o;
          unf->o=ss->dal;
          ss->dal=ss->dal->dal;
          delete unf->o;
        }
        break;
      case _Lseznamovapromenna:
        if(unf->p){
          ss=unf->o;
          ss->u1=unf->lok.s->ss1;
          ss->u2=unf->lok.s->ss2;
          if(ss->u2==NULL){
            merr:
            if(unf->lok.s->q!=NIL) unf->lok.s->q->pocminus();
            unf->p->obsah=NULL;
            delete unf->lok.s;
            break;
          }
          if(unf->lok.s->u==NIL){
            unf->lok.s->u=new Qstrom(ss->u2->vjmeno(),ss->u2->vkonst());
	    if(!unf->lok.s->u){ ERR; goto merr; }
            unf->lok.s->u->vjmeno()->zvys();
            if(ss->u2->vsyn()) unf->lok.s->u->nsyn(ss->u2->adsyn());
            unf->lok.s->q=unf->lok.s->u;
          }else{
            unf->lok.s->u->nbratr(new Qstrom(ss->u2->vjmeno(),ss->u2->vkonst()));
	    if(!unf->lok.s->u->vbratr()){ ERR; goto merr; }
            unf->lok.s->u->vbratr()->vjmeno()->zvys();
            unf->lok.s->u=unf->lok.s->u->vbratr();
            if(ss->u2->vsyn()) unf->lok.s->u->nsyn(ss->u2->adsyn());
          }
          ss->u2=ss->u2->vbratr();
          unf->p->obsah=unf->lok.s->q;
          unf->lok.s->ss1=ss->u1;
          unf->lok.s->ss2=ss->u2;
          goto dal;
        }else{
          ss=unf->o;
          while(ss->dal!=unf->lok.s->s){
            unf->o=ss->dal;
            ss->dal=ss->dal->dal;
            delete unf->o;
          }
          delete unf->lok.s;
        }
        break;
      case _Ldekompozice:
        ss=unf->o;
        ss->u1=unf->lok.d->ss1;
        ss->u2=unf->lok.d->ss2;
	// !!!
	//fprintf(stderr, "3 %s %d\n", unf->lok.d->s, !ss->u2 ? 9999 : strlen(ss->u2->vobsah())); //, *(ss->u2->vobsah()));
        if(ss->u2&&!ss->u2->vsyn()&&strlen(ss->u2->vobsah())==1&&isid(*(ss->u2->vobsah()))){
          unf->lok.d->s[unf->lok.d->i++]=*(ss->u2->vobsah());
          unf->lok.d->s[unf->lok.d->i]=0;
          unf->lok.d->q->nobsah(unf->lok.d->s);
	  //fprintf(stderr, "4 %s\n", unf->lok.d->s);
          ss->u2=ss->u2->vbratr();
          unf->lok.d->ss1=ss->u1;
          unf->lok.d->ss2=ss->u2;
          goto dal;
        }
        unf->lok.d->q->pocminus();
        unf->p->obsah=NULL;
        delete unf->lok.d;
        break;
      case -1:
        ss=unf->o;
        ss->dal->u1=unf->lok.k->p1;
        ss->dal->u2=unf->lok.k->p2;
        delete unf->lok.k;
        break;
    }
    pun=unf;
    unf=unf->zpet;
    delete pun;
    goto zpet;
  }
}

//Hodilo by se provazani pravidla obema smery ... doplnil jsem ho tam
void pouzij(Qpravidlo *pr,Qhrana *u){
  Qhrana *l=pr->levyretez();
  Bpromsez *ps=NULL;
  seznam_promennych(&ps,l);MER;
  Bsezsez *ss=new Bsezsez;
  if(!ss) ERR;
  else{
    ss->u1=l->vstrom();
    ss->u2=u->vstrom();
    ss->dal=NULL;
    int uzito=0;
    unifikuj(ss,ps,l,u,u,pr,uzito);
    delete ss;
  }
  zrus_seznam_promennych(ps);
}

void nulovani_seznamu(Qhrana *st){
  while(st){
    st->nurov(0);
    st=st->dal();
  }
}

void maz(Qhrana *q){
  q->nretez1(NULL);
  q->nvetev1(NULL);
  if(unik&&q->pocitadlo()==1&&q->vstrom()&&q->vstrom()->pocitadlo()==1) unik->zrus(q->vstrom());
  q->pocminus();
}

void cisteni(Qhrana *&start,Qhrana *&konec){
  int jeste;
  Qhrana *u,*v=NULL,*w=NULL,*wk,*s=konec,*p;
  do{
    jeste=0;
    u=s;
    v=NULL;
    while(u) if(u->vpouz()){
      int pryc=1;
      if(!u->vvetev1()){
        p=u->vretez2()?u->vretez2()->vretez1():start;
        while(p&&p->vpouz()) p=p->vvetev1();
        if(p) pryc=0;
        else{
          if(u->vretez2()){
            if(!(u->vpouz()&2)){
              u->npouz(u->vpouz()|2);
              for(p=u->vretez2();p;p=p->vvetev2()) p->npouz(p->vpouz()|1);
              jeste=1;
            }
          }else{
/*            start->pocminus();
            start=konec=NULL;
            return;/**/
            if(Bprazdnygraf){
              start->pocminus();
              start=konec=NULL;
              return;
            }else{
              if(w){
                wk->ndalsi(s);
                s=w;
                w=NULL;
              }
              u=s;
              while(u){
                u->npouz(u->vurov()==0?0:1);
                u=u->dal();
              }
              jeste=0;
              break;
            }
          }
        }
      }
      if(!u->vvetev2()){
        p=u->vretez1()?u->vretez1()->vretez2():konec;
        while(p&&p->vpouz()) p=p->vvetev2();
        if(p) pryc=0;
        else{
          if(u->vretez1()){
            if(!(u->vpouz()&4)){
              u->npouz(u->vpouz()|4);
              for(p=u->vretez1();p;p=p->vvetev1()) p->npouz(p->vpouz()|1);
              jeste=1;
            }
          }else{
/*            start->pocminus();
            start=konec=NULL;
            return;/**/
             if(Bprazdnygraf){
              start->pocminus();
              start=konec=NULL;
              return;
            }else{
              if(w){
                wk->ndalsi(s);
                s=w;
                w=NULL;
              }
              u=s;
              while(u){
                u->npouz(u->vurov()==0?0:1);
                u=u->dal();
              }
              jeste=0;
              break;
            }
         }
        }
      }
      if(pryc){
        if(v){
          v->ndalsi(u->dal());
          u->ndalsi(w);
          if(!w) wk=u;
          w=u;
          u=v->dal();
        }else{
          s=u->dal();
          u->ndalsi(w);
          if(!w) wk=u;
          w=u;
          u=s;
        }
      }else{
        v=u;
        u=u->dal();
      }
    }else{
      v=u;
      u=u->dal();
    }
  }while(jeste);
  if(w){
    wk->ndalsi(s);
    s=w;
  }
  u=s;
  while(u){
    if(!u->vvetev1()){
      p=u->vretez2()?u->vretez2()->vretez1():start;
      while(p&&p->vpouz()) p=p->vvetev1();
      if(u->vretez2()) for(v=u->vretez2();v;v=v->vvetev2()) v->nretez1(p);
      else start=p;
      v=p;
      while(p){
        for(p=p->vvetev1();p&&p->vpouz();p=p->vvetev1());
        v->nvetev1(p);
        v=p;
      }
    }
    if(!u->vvetev2()){
      p=u->vretez1()?u->vretez1()->vretez2():konec;
      while(p&&p->vpouz()) p=p->vvetev2();
      if(u->vretez1()) for(v=u->vretez1();v;v=v->vvetev1()) v->nretez2(p);
      else konec=p;
      v=p;
      while(p){
        for(p=p->vvetev2();p&&p->vpouz();p=p->vvetev2());
        v->nvetev2(p);
        v=p;
      }
    }
    u=u->dal();
  }
  u=s;
  while(u){
    if(u->vpouz()){
      p=u;
      u=u->dal();
      maz(p);
    }else{
      p=u;
      u=u->dal();
      p->ndalsi(NULL);
    }
  }
}

/*
  Predpoklady:
    ve vsech Quzlech grafu je pouzito=0
    start i konec ukazuji na prvniho v seznamu uzlu vedoucich z pocatku a do konce
*/
void beh(Qhrana *&start,Qhrana *&konec,Qprogram *prg){
  Qfaze *fz=prg->faze();
  while(fz&&start){
    S=start;
    K=konec;
    Qhrana *u;
    log.fz=fz->vid();
    if(log.f) fprintf(log.f,"(%i. faze)\n",log.fz);
    serad_uzly(konec);
    u=konec;
    while(u){
      Qpravidlo *pr=fz->pravidlo();
      while(pr){
        pouzij(pr,u);
        MEM;
        pr=pr->dal();
      }
      MEM;
      u=u->dal();
    }
    MEM;
    if(log.f&&Bgraflog){
      fprintf(log.f,"(graf pred cistenim)\n");
      nulovani_seznamu(start);
      zapis_log_grafu(start);
      MEM;
    }
    cisteni(start,konec);
    fz=fz->dal();
  }
}

int Qprogram::beh(Qvstup *vst,FILE *f){
  memerr=0;
  NIL=new Qstrom("",0);
  if(!NIL) { MERR; return 1; }
  log.f=f;
  unsigned long n=0;
  while(vst){
    Qhrana *s,*k;
    s=k=vst->vhrana();
    if(!s) break;
    while(s->vretez2()) s=s->vretez2();
    while(k->vretez1()) k=k->vretez1();
    if(log.f&&Bgraflog){
      fprintf(log.f,"\n(%lu. vstup)\n",++n);
      zapis_log_grafu(s);
      MEM;
    }
    unik=vst->vunik();
    ::beh(s,k,this);
    vst->nhrana(s);
    if((!s)&&unik) {delete vst->vunik(); vst->nunik(NULL);}
    MEM;
    if(log.f&&Bgraflog){
      fprintf(log.f,"(%lu. vystup)\n",n);
      zapis_log_grafu(s);
      MEM;
    }
    vst=vst->dalsi();
  }
  delete NIL;
  if(memerr) MERR;
  return memerr;
}
